\newcommand{\Lang}{\textbf{HC}}
\section{The   languages  \textbf{HC} and \textbf{PHC}}\label{sec:language}

In this section we define \textbf{HC}, our core functional language, and
 \textbf{PHC}, the language of properties over \textbf{HC} terms.

\subsection{The core functional language \textbf{HC}}

\textbf{HC}, defined in \fig{hcdef}, is a minimal non-polymorphic\footnote{Zeno does in fact support polymorphism but we have removed it here for simplicity.} subset of Haskell and can be run by any Haskell98\cite{haskell98} compliant compiler. We use  \li{x} for variable names, \li{f} for function names, \li{K} for constructor names, and  \li{T} for type names. In \fig{exdefs}
we give a working example.


A function definition, $FunDef$,  introduces a new function \li{f} with 0 or more parameters, $\lim{x}^*$. Lines 9 and 10  in \fig{exdefs} define a function \li{add}  with parameters \li{n} and \li{m}.
%
A term,  $\tau$,  is a   variable (\li{x}), or a function (\li{f}), or a constructor (\li{K}), or the \emph{application} of a \emph{function term} ($\tau_1$) to an \emph{argument term} ($\tau_2$). Term application is implicitly left-associative, e.g., $\lim{f x y} \equiv \lim{((f x)}\ \lim{y)}$.
%
An expression, $Expr$,  is   a term ($\tau$), or the \emph{case-analysis} of another term ($\caseof{\tau}{\lim{...}}$) giving one of many $Alt$ernative expressions depending on the value of the term being analysed.
%
A type, $\type$,   is either a type name \li{T} or a function type  $\type_1\ \lim{->}\ \type_2$. Function types are implicitly right-associative, e.g., \li{Nat -> Nat -> Nat} $\equiv$ \li{(Nat -> (Nat -> Nat))}.
%
A $TypeDef$ introduces a new type name \li{T}, and  one or more constructors $\lim{K}$.
The constructors take  0 or more arguments of a given type. 

Although not represented in our grammar, if a function is an operator surrounded by parentheses, it can be used infix without the parentheses, e.g., $\lim{x + y} \equiv \lim{(+) x y}$. 

% When a constructor has one or more arguments of the same type as the one to which it belongs, we call it a {\em recursive constructor.} For example, \li{Suc}  defined on line 5 of \fig{exdefs} is a recursive constructor.

% $FunType$ is an annotation which defines the type of a function \li{f} to be $\type$. On line 13 of our example in \fig{exdefs} we define the type of our less-than-or-equal function to take two \lit{Nat} arguments and return a \li{Bool}.
% sd removed: too obvious

\begin{figure}[tb]
\small
\begin{lstlisting}[numbers=left]
-- Boolean datatype, either True or False
data Bool = True | False

-- Natural numbers as a recursive datatype
data Nat  = 0 | S Nat

-- Addition function on natural numbers
(+) :: Nat -> Nat -> Nat
n + m = case n of { 0 -> y;
                    S n' -> S (n' + m) }

-- Less-than-or-equal-to function on natural numbers
(<=) :: Nat -> Nat -> Bool
n <= m = case n of { 0 -> True ;
                     S n' -> case m of {
                        0 -> False ;
                        S m' -> n' <= m' } }
	
-- Returns the largest of two numbers
max :: Nat -> Nat -> Nat
max n m = case n <= m of { True -> m; False -> n }
\end{lstlisting}
\caption{Example types and functions in \textbf{HC}}
\label{fig:exdefs}
\end{figure}

% \subsection{Evaluating expressions in \textbf{HC}}
% \label{sec:eval}

 Execution of \textbf{HC} expressions is defined by the judgement  ($E_1 \leadsto E_2$), given in \fig{evalexpr}.
  In \fig{evalex} we  show
  the evaluation of \li{(S 0)} \li{+ 0} to \li{S 0}.
 % SD cur, doh? , i.e. $1 + 0 = 1$.

\begin{figure}[h]
%\inferrule{
%}{
%flatten (\lim{x}) = \lim{x} \\
%flatten (\lim{K}) = \lim{K} \\
%flatten (\tau_1\ \tau_2) = (flatten (\tau_1))\ \tau_2
%}
%\]

%\[
%\inferrule{
%\tau_1 \leadsto \tau_2
%}{
%(\tau_1\ \tau_3) \leadsto (\tau_2\ \tau_3)
% \\
% (\tau_3\ \tau_1) \leadsto (\tau_3\ \tau_2)
%}
%\]
%\\
\[
\inferrule{
% \lim{f}\ \vect{\tau_a} = flatten(\tau) \\
(\lim{f}\ \vect{\lim{x}}\ \lim{=}\ E) = definition(\lim{f})
}{
\lim{f}\ \vect{\tau_a} \leadsto E[\vect{\tau_a / x}]
}
\]
\\
\[
\inferrule{
% \lim{K}\ \vect{\tau_a} = flatten(\tau) \\
(\lim{K}\ \vect{\lim{x}}\ \lim{->}\ E) \in \vect{A}
}{
\caseof{\lim{K}\ \vect{\tau_a}}{\vect{A}} \leadsto E[\vect{\tau_a / x}]
}
\]
\\
\[
\inferrule{
\tau_1 \leadsto \tau_2
}{
\caseof{\tau_1}{\vect{A}} \leadsto \caseof{\tau_2}{\vect{A}}
}
\]
  \caption{Expression evaluation in \textbf{HC}}
  \label{fig:evalexpr}
  \end{figure}

\begin{figure}[h]
 \begin{align*}
& \lim{(S 0)}\ \lim{+ 0} \\
& \leadsto \caseof{\lim{(S 0)}}{\lim{...; S n' -> S (n' + 0)}} \\
& \leadsto \lim{S (0 + 0)} \\
& \qquad \qquad \ \lim{0 + 0} \\
& \qquad \qquad \ \leadsto \caseof{\lim{0}}{\lim{0 -> 0; ...}} \\
& \qquad \qquad \ \leadsto \lim{0} \\
& \leadsto \lim{S 0}
\end{align*}
\caption{Evaluation of \li{(S 0)} \li{+ 0}}
\label{fig:evalex}
\end{figure}


\subsection{The properties language \textbf{PHC}}

\begin{figure}[h]
\small
\begin{align*}
& \varphi & ::= & \quad \tau_1 = \tau_2 \\
& Prop & ::= & \quad \varphi \quad | \quad \varphi\ \lim{:-}\ \varphi\ (\lim{,}\ \varphi)^*
\end{align*}
\caption{\textbf{PHC} syntax}
\label{fig:funpropdef}
\end{figure}

The language \textbf{PHC}, whose syntax is given in \fig{funpropdef}, supports
definite clauses of equality between terms under universal quantification.
 We follow a Prolog-style   notation whereby $\equality\ \lim{:-}\ \equalities$
 stands for %
 %``$\equality$ is implied by $\equalities$'' i.e.
 $\equalities \Rightarrow \equality$, and a comma \li{,} stands for ``and'' ($\wedge$).
 We   %often
 refer to the property we are attempting to prove  as the \emph{goal}.
 We refer to the $\equality$ to the left of the \li{:-} as the \emph{consequent}, and the $\equalities$ to the right of the \li{:-} as the \emph{antecedents} or \emph{conditions}.

Note  that the term  $\lim{True}$   is not logical truth; it is just one constructor of the two constructor data type \li{Bool}.
It is possible to express full propositional logic in our syntax, since we can express its operators as functions in \textbf{HC} using the data type \li{Bool}. However, it  is not possible to express FOL, as we have no way of expressing existential quantification, nor can we express   nested universal quantification.

All variables within a property that are not constructors or defined functions are implicitly universally quantified. For example,
 \\
 $ ~ $ \ \ \hspace{.5in}  
 % take the transitivity of \li{leq} (see \fig{exdefs} for definitions):
\li{x <= z = True :- x <= y = True, y <= z = True}\\
expresses the transitivity of \li{(<=)}, i.e., that
 \\
  $ ~ $ \ \ \hspace{.5in}  
\ $\forall x. \forall y. \forall z.\ \big[\ (x\ \lim{<=}\ y = \lim{True}) \wedge (y\ \lim{<=}\ z = \lim{True})\ \big] \Rightarrow (x\ \lim{<=}\ z = \lim{True})\   $.



